l,l2:IdLnk, dt:fpf(Id; tg.Type), tg:Id.
(fpf-dom(Kind-deq; rcv(l2,tg); lnk-decl(l; dt)))  (l2 = l) 

latex

Definitions	P  Q, t  T, guard(T), P  Q, x:A. B(x), x:A. B(x), IdLnk, Id, rcv(l,tg), Knd, P  Q, map(f; as), Kind-deq, b, fpf-dom(eq; x; f), lnk-decl(l; dt), fpf(A; a.B(a)), x. t(x), top
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, lnk-decl wf, fpf wf, IdLnk wf, assert-deq-member, Kind-deq wf, map wf, member map, Knd wf, rcv wf, Id wf, rcv one one